$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{N}\rightarrow$Prop).
\\[0ex]($\forall$$s$:$A$. Dec($\exists$$k$:$\mathbb{N}$. $\neg$$P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:$A$, $k$:$\mathbb{N}$. Dec($P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:$A$. Dec($\exists$$v$:$\mathbb{N}$. $\neg$$P$($s$,$v$) \& ($\forall$$n$:$\mathbb{N}$. $n$$<$$v$ $\Rightarrow$ $P$($s$,$n$))))